T:Type{i}, S:((T)Prop{i'}).
(i:. generic{i:l}(T; x.S(i,x)))  generic{i:l}(T; x.(i:. S(i,x))) 

latex

Definitions	Generic{f:T|S(f)}, Type, t  T, Prop, , x:AB(x), f(a), x(s1,s2), x. t(x), x:A. B(x), P  Q, x:AB(x), Surj(A; B; f), x:A. B(x), ||as||, P & Q, i  j < k, a<b, False, A, AB, , {x:A| B(x) }, {i..j}, #$n, Void, l[i], s = t, type List, l1  l2, 1of(t), A/x,y. B(x;y), x.A(x), <a,b>, A & B, {T}, SQType(T), s ~ t, True, T, 2of(t)
Lemmas	pi2 wf, nat sq, pi1 wf, iseg wf, int seg wf, select wf, le wf, length wf1, pair-coding-exists, generic wf, nat wf